IrrelevantProjections.agda:15,10-17
Identifier inflate is declared irrelevant, so it cannot be used
here
when checking that the expression inflate x has type A
